\begin{tabbing} $\forall$\=${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \},\+ \\[0ex]$Q$:(\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}$\rightarrow$\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}$\rightarrow$Prop). \-\\[0ex]$e_{1}$ $\leq$ $e_{2}$ $\Rightarrow$ $Q$($e_{1}$,$e_{2}$) $\Rightarrow$ [$e_{1}$,$e_{2}$]$\sim$([$a$,$b$].$Q$($a$,$b$))+ \end{tabbing}